M:MsgA, a:Id, s:M.state. unsolvable M.pre(a,s)  Prop 

latex

Definitions	MsgA, M.state, unsolvable M.pre(a,s), M.da(a), z != f(x)  P(a;z), b, x  dom(f), IdDeq, f(x)?z, Knd, KindDeq, Top, A, f(x), P  Q, a:A fp B(a), x. t(x), locl(a), Prop, State(ds), x:A. B(x), Id, Valtype(da;k), t  T
Lemmas	Id wf, ma-state wf, locl wf, ma-valtype wf, fpf-trivial-subtype-top, fpf-ap wf, not wf, top wf, Kind-deq wf, Knd wf, fpf-cap wf, id-deq wf, fpf-dom wf, assert wf, msga wf